\section{Related Work}
\label{sec:related}


Various techniques have been proposed on regression testing of software programs~\cite{Rothermel:1996:ART:235681.235682, Graves:2001:ESR:367008.367020}.
These techniques aim to select test cases that could reveal different behaviors after modification
in programs.
%These techniques are related to regression-test selection \cite{Rothermel:1996:ART:235681.235682}, 
%\cite{Graves:2001:ESR:367008.367020}, and test-suite prioritization \cite{Elbaum:2000:PTC:347324.348910}.
Note that these techniques focus on changes at code level.
None of these techniques consider potential changes that can arise from code-related components (such as security policies specified separately).
Polices and general programs are fundamentally different in terms of structures, semantics, and
functionalities, etc. Therefore, techniques for regression
testing of programs are not suitable for addressing 
the test-selection problem for policy evolution.
%Our work is the first automatic test-selection approach for policy
%evolution.
\Comment{
Prior work that is closest to ours is Mouelhi et al.'s
work~\cite{mouelhi09:tranforming}.
They proposed a technique to transform functional test cases into security test cases. 
These test cases then be used to verify correctness of access control mechanisms in policy-based systems.
They defined various mutation operators at the policy level.
Given a policy and its mutated policy, the technique selects only impacted test cases to be transformed as security test cases
(with additional manual task to add code for checking security).
While this work focuses on security test case selection from initial test cases,
our work focuses on test selection problem impacted by policy changes
to reveal faults induced by policy changes.
}

Another approach closest to ours is Fisler et al.'s
approach~\cite{fisler05:verification}.
They developed a tool called Margrave that enables conducting change-impact analysis between two XACML
policies. We could use Margrave to identify semantic policy changes
between two policies.
However, Margrave does not support test selection as our work does.
% However, Margrave supports for only limited functionality of XACML. Moreover, 


%where system behaviors are changed by policy evolution as
%our work does.


%does not supports for functionality of XACML sufficiently
%and  
%
%limited functionality of XACML
%policies
%
%Margrave does not handle with situations where
%program behaviors are changed by policy changes as our work focuses on.
%Moreover, Margrave supports limited functions of XACML, and 

%in terms of regression testing. As application
%code can often interact with policies, our work is useful

\Comment{
To facilitate verifying and validating the correctness of policies, prior
research work has been done in the area of policy testing, which generates and executing test requests against a policy.
Martin et al.~\cite{martin06:defining} proposed a framework to detect policies faults by analyzing
policy test suites that involve 
requests-responses pairs. The framework is based on mutation operators~\cite{martin07:fault} that enable measuring fault detection capability. 
It uses a tool~\cite {martin07:automated} that aims at minimizing the test cases to be generated by analyzing the structural coverage of the policies.
Hu et al.~\cite{hu07:conformance} proposed a generic model-based conformance checking technique for access control policies written in
XACML.
These approaches focus on test request generation at a policy level (e.g., policies written in XACML).
Instead of generating new requests, our work focuses on regression testing at the implementation level (the system level) by
reusing existing hardcoded test cases.
}
%, which includes
%application code when a policy evolves. 


%Margrave detects the presence of requests that may violate the specified properties.

%used these mutated policies to select impacted tests. The impacted tests are then tranformed to security tests (by added specific code to check the security mechanism). 
%Although this work focused on applications interacting with policies, it was not presented from a regression testing perspective.
%
%
%The most relevant paper that is related to our work was presented by Mouelhi et al. in~\cite{mouelhi09:tranforming}. The authors proposed transforming functional tests into security tests. 
%These tests can then be used to validate the access control mechanisms in policy-based systems. They defined mutation operators at the policy level and used these mutated policies to select impacted tests. The impacted tests are then tranformed to security tests (by added specific code to check the security mechanism). 
%Although this work focused on applications interacting with policies, it was not presented from a regression testing perspective. 

%fault
%localization problem of ?rewall policies.
%
%This paper focuses on regression testing for policy-based software systems.

 


%Zhang et al \cite{DBLP:conf/isw/ZhangRG05} used model checking technique which is supported by a tool to evaluate access
%control policies specified in a modelling formalism called RW. Hughes et al. \cite{hughes04:automated} proposed using First-Order Logic 
%to automatically verify access control policies. Their model is based on specifying access to resources, they show that the access
%control policies in XACML can be translated into a normlized form that includes four classes: permit,
%deny, error, and not-applicable. A partial ordering among access control polices enable the authors to specify properties that are checked later
%with Alloy analyszer \cite{Alloy}. Nyanchama et. al. \cite{Nyanchama99therole} focused on policy analysis and verification related to 
%RBAC models. They used graphs to model hierarchies of users, roles and permissions and to solve role-role conflicts issues.
%While these different approaches focus on test request generation for validating the policy implementation (the XACML code), 
%the technique presented in this paper focuses on regression testing at the implementation level (the system level) which occurs when the access control policy evolves. 





\Comment{
Our previous work~\cite{hu10:model,hu08:property} presented
model checking to verify various policies such as role-based
access control policies~\cite{ferraiolo92:role}.
Our previous work translates policies into specifications
in NuSMV~\cite{cimatti02:nusmv2}. NuSMV verifies the specifications against properties. 
Based on our previous work, we developed a tool, called ACPT\footnote{http://csrc.nist.gov/groups/SNS/acpt/index.html},
to verify and test access control policies.
However, our previous work does not detect conflicts
or redundancies between two policies, one major
focus of our current work. Moreover, our previous
work does not recommend any combinations (to the policy
authors) that can be recommended by our current work. 

There exist tools to verify XACML policies. These tools require XACML policies in formal specification languages such as 
Alloy~\cite{jackson01:micromodularity}. Hughes et al.~\cite{hughes04:automated} proposed an approach to translate XACML policies to a model 
specified in the Alloy language~\cite{jackson01:micromodularity}. Then, the Alloy Analyzer verifies whether the model satisfies the given properties.
Kolovski et al.~\cite{kolovski07:analyzing} converted XACML policies into specifications in  description logics (DL) and adopted existing DL 
verification tools to verify the specifications. Fisler et al.~\cite{fisler05:verification} developed a Binding Decision Diagram (BDD) based 
verification tool, called Margrave, to verify XACML policies. Margrave parses XACML policies into the BDD structure. Moreover, Margrave supports 
change-impact analysis to report which decisions are changed after policy modification.
Similar to these previous approaches, our approach focuses on modeling and verifying policies via a symbolic model checking. Moreover, our approach
 verifies whether two policies may include conflicts and redundancies via a symbolic model checking. 
While these previous approaches do not help combining two policies, our approach recommends combinations of two policies that could satisfy 
user-specified properties. 


%\textbf{Policy Combinations/Integration.}
%Bonatti et al.~\cite{Bonatti2} proposed combining sub-policies based on 2-valued algebra. 
Backes et al.~\cite{backes04algebra} proposed a 3-valued algebra to combine sub-policies considering privacy policies.
 They defined relations of combination with three operators: conjunction, disjunction, and scoping.
 Li at el.~\cite{Ninghui2009} proposed an algebra for combining sub-policies. 
They introduced new combining algorithms such as weak majority or strong majority.
For example, in the case of the strong majority combining algorithms, at least 2/3 
rules evaluated against a request should be evaluated to the same decision. Since the decision is the majority, 
the decision is returned as a final decision. They proposed algebras to generalize their combining algorithms.
%Mazzoleni et al.~\cite{Mazzoleni2006} proposed policy integration that can be applied to XACML policies. 
In their approach, policy authors can specify conditions to represent how their policies can be integrated with other policies. 
Their integration approach is based on analysis of two policies to be integrated. Policy authors measure similarity of two policies 
and integrate the policies based on given condition.





}
\Comment{
%\textbf{Policy Change Impact Analysis}
%\textbf{Policy Conflict and Redundancy}
%\textbf{Verification in NuSMV for other projects}

%interaction, but runtime ...more general stuff to do it.

\textbf{Policy Verification.}
There are verification tools available for XACML
policies. Hughes et
al.~\cite{hughes04:automated}
proposed an approach
to verify XACML policies by
translating the policies to the Alloy
language~\cite{jackson01:micromodularity}.
Then, they use Alloy Analyze to verify properties
against the translated policies. 
Zhang et
al.~\cite{zhang05:evaluating} developed a model-checking tool
to verify policies specified in
\Intro{RW} languages~\cite{zhang04:synthesis}, which can be converted to
XACML.
Kolovski et
al.~\cite{kolovski07:analyzing} formalize XACML policies with
description logics (DL), which are a decidable fragment of
first-order logic, and exploit existing DL verifiers to conduct
policy verification.
Schaad and Moffett~\cite{schaad02:lightweight} leverage
Alloy~\cite{jackson01:micromodularity} to check that role-based
access-control policies do not allow roles to be assigned to users
in ways that violate SoD constraints.
Similar to previous research work, our work also model and verify policies
via model checking. However, we extend
our work to detect conflict and redundancy via a symbolic checker.


\textbf{Policy Combinations/Integration.}
Bonatti et al.~\cite{Bonatti2} proposed combining sub-policies based on 2-valued algebra. Backes et al.~\cite{backes04algebra} proposed a 3-valued algebra to combine sub-policies considering privacy policies. They defined relations of combination with three operators: conjunction, disjunction, and scoping. Li at el.~\cite{Ninghui2009} proposed an algebra for combining sub-policies. They also introduce new combining algorithms such as weak majority or strong majority. For example, in case of the strong majority combining algorithms, at least 2/3 rules evaluated against a request should return the same decision. As the decision is majority, the decision is returned as a final decision. They propose algebras to generalize their combining algorithms. Moreover, they propose combinations of sub-policies, which may return policy evaluation errors and obligations.
Mazzoleni et al.~\cite{Mazzoleni2006} proposed policy integration that can be applied to XACML policies. In their approach, policy authors can specify conditions to represent how their policies can be integrated with other policies. Their integration approach is based on analysis of two policies to be integrated. Policy authors measure similarity of two policies and integrate the policies based on given condition.
We also propose that a methodology to combine two policies using property verification.
We next describe a methodology to recommend the combinations (of two policies) that could satisfy user-specified properties.

\textbf{Policy Testing.}

Our previous work~\cite{hu10:model} demonstrated an approach
to represent a policy and its properties as
corresponding finite state machine (FSM) model and temporal
logics (e.g., computation tree logic), respectively, using SMV specification language~\cite{cimatti02:nusmv2}.

Our previous work developed policy testing approaches for policy
structural coverage~\cite{martin06:defining}, request
generation~\cite{martin07:automated}, and mutation
testing~\cite{martin07:fault}.
% Our previous
%work~\cite{hu07:conformance} also proposed a generic model-based
%conformance checking approach for access control policies written in
%XACML.
These pieces of work do not rely on properties for generating
test requests to detect a fault in a policy. 
Our previous work~\cite{martin08:assessing} developed an approach
for measuring the quality of policy properties in policy
verification. Given user user-specified
properties, the quality of properties are measured
based on fault-detection capability.
}